In integrated circuit and hardware design, verification refers to the process of proving that a design satisfies its specification. For example, digital logic circuits implement a logic function and represent the core of any computing processing unit. These designs are often of substantial complexity, comprising a diversity of bit-level control logic, data paths, and performance-related artifacts including pipelining, multi-threading, out-of-order execution, and power-saving techniques. Memory arrays are ubiquitous in hardware designs, representing caches, main memory, lookup tables, and the like.
Before a logic design is constructed in real hardware, its design is tested and the operation thereof verified against a design specification. Typically, the specification of a verification problem includes a netlist-based representation of the design and a set of expected values for specified nets under specified conditions. However, verification techniques generally require computational resources which are exponential with respect to the size of the design under test. In particular, many formal analysis techniques require exponential resources with respect to the number of state elements in the design under test. Thus, it's often desirable to reduce the complexity of a design under verification. For example, abstraction techniques may be used to reduce memory array sizes (e.g., to reduce the number of rows which need to be modeled), to enable reductions in the size of the netlist under verification, and thereby reduce verification complexity.